$\forall$$A$, $B$:Type, $g$:($A$$\rightarrow$($B$ + Top)), $X$:MaInterface($A$), ${\it es}$:ES.
\\[0ex]ma{-}interface{-}consistent(${\it es}$;$X$)
\\[0ex]$\Rightarrow$ ([[ma{-}interface{-}compose($g$;$X$)]] = $g$ o [[$X$]]   $\in$ AbsInterface($B$))